;;;===========================================================================
;;;
;;; Simplicial Algebraic Topology Macros
;;;
;;;---------------------------------------------------------------------------
;;;
;;; JHV: 
;;;
;;; Start date: 24/04/10 || End date: 03/05/10
;;;
;;;===========================================================================

(in-package "ACL2")

(include-book "algebraic-structures")

;;;***************************************************************************
;;;
;;; Graded R-module
;;;
;;;***************************************************************************


(defun closure-operation-abelian-group (inv group-operation)
   `(implies (and (,inv n a) 
		  (,inv n b)
		  (integerp n))
	    (,inv n (,group-operation n a b))))

(defun commutativity (inv group-operation)
    `(implies (and (,inv n a) 
		   (,inv n b)
		   (integerp n))
	    (equal (,group-operation n a b)
		   (,group-operation n b a))))

 (defun associativity-operation-abelian-group (inv group-operation)
    `(implies (and (,inv n a)
		   (,inv n b)
		   (,inv n c)
		   (integerp n))
	    (equal (,group-operation n (,group-operation n a b) c)
		   (,group-operation n a (,group-operation n b c)))))
 
 (defun closure-zero-element (inv zero-elem)
    `(,inv n (,zero-elem n)))

 (defun closure-external-abelian-group (inv inv-ring external)
    `(implies (and (,inv n a)
		   (,inv-ring r)
		   (integerp n))
	    (,inv n (,external n r a))))

 (defun existence-identity-element (inv group-operation zero-elem)
    `(implies (and (,inv n a) (integerp n))
	    (equal (,group-operation n a (,zero-elem n))
		   a)))

 (defun closure-inverse-element (inv inverse)
    `(implies (and (,inv n a) (integerp n))
	    (,inv n (,inverse n a))))

(defun group-operation-inverse (inv group-operation inverse)
  `(implies (and (,inv n a)
		 (,inv n b)
		 (integerp n))
	   (equal (,inverse n (,group-operation n a b))
		  (,group-operation n (,inverse n a) (,inverse n b)))))

(defun unicity-inverse-element (inv group-operation zero-elem inverse)
    `(implies (and (,inv n a)
		   (,inv n b)
		   (integerp n)
		   (equal (,group-operation n a b) (,zero-elem n)))
	    (equal (,inverse n a) b)))

 (defun existence-inverse-element (inv group-operation inverse zero-elem)
    `(implies (and (,inv n a) (integerp n))
	    (equal (,group-operation n a (,inverse n a))
		   (,zero-elem n))))
  

 (defun distributivity-external-law-1 (inv inv-ring external group-operation)
    `(implies (and (,inv n a)
		   (,inv n b)
		   (,inv-ring r)
		   (integerp n))
	    (equal (,external n r (,group-operation n a b))
		   (,group-operation n (,external n r a)
				    (,external n r b)))))

 (defun distributivity-external-law-2 (inv inv-ring external addition-ring group-operation)
    `(implies (and (,inv n a)
		 (,inv-ring s)
		 (,inv-ring r)
		 (integerp n))
	    (equal (,external n (,addition-ring s r) a)
		   (,group-operation n (,external n s a)
				  (,external n r a)))))

 (defun distributivity-external-law-3 (inv inv-ring external product-ring)
    `(implies (and (,inv n a)
		 (,inv-ring s)
		 (,inv-ring r)
		 (integerp n))
	    (equal (,external n (,product-ring s r) a)
		   (,external n s (,external n r a)))))

 (defun identity-external (inv external unit)
    `(implies (and (,inv n a) (integerp n))
	    (equal (,external n (,unit) a)
		   a)))

(defun external-inverse (inv inv-ring external inverse)
  `(implies (and (,inv n a)
		 (,inv-ring s)
		 (integerp n))
	   (equal (,inverse n (,external n s a))
		  (,external n s (,inverse n a)))))


(defun external-zero (inv-ring external zero)
  `(implies (and (,inv-ring s)
		 (integerp n))
	   (equal (,external n s (,zero n))
		  (,zero n))))


(defun inverse-zero (inverse zero)
  `(implies (integerp n)
	    (equal (,inverse n (,zero n))
		   (,zero n))))


(defun graded-r-module-condition (inv-ring addition-ring zero-elem-ring inverse-ring product-ring unit-ring
				inv-cc group-operation-cc zero-elem-cc external-cc inverse-cc)
  (cons 'and 
	(cons (ring-algebraic-structure inv-ring addition-ring zero-elem-ring inverse-ring product-ring unit-ring)
	      (cons (closure-operation-abelian-group inv-cc group-operation-cc)
		    (cons (associativity-operation-abelian-group inv-cc group-operation-cc)
			  (cons (closure-zero-element inv-cc zero-elem-cc)
				(cons (closure-external-abelian-group inv-cc inv-ring external-cc)
				      (cons (existence-identity-element inv-cc group-operation-cc zero-elem-cc)
					    (cons (closure-inverse-element inv-cc inverse-cc)
						  (cons (unicity-inverse-element inv-cc group-operation-cc zero-elem-cc inverse-cc)
							(cons (existence-inverse-element inv-cc group-operation-cc inverse-cc zero-elem-cc)
							      (cons (commutativity inv-cc group-operation-cc)
								    (cons (distributivity-external-law-1 inv-cc inv-ring external-cc group-operation-cc)
									  (cons (distributivity-external-law-2 inv-cc inv-ring external-cc addition-ring group-operation-cc)
										(cons (distributivity-external-law-3 inv-cc inv-ring external-cc product-ring)
										      (cons (identity-external inv-cc external-cc unit-ring)
											    (cons (group-operation-inverse inv-cc group-operation-cc inverse-cc)
												  (cons (external-inverse inv-cc inv-ring external-cc inverse-cc)
													(cons (inverse-zero inverse-cc zero-elem-cc)
													      (cons (external-zero inv-ring external-cc zero-elem-cc)
											    'nil))))))))))))))))))))

	      

  
;;;***************************************************************************
;;;
;;; Morphism degree -1
;;;
;;;***************************************************************************

 
 (defun closure-function--1 (inv-source inv-target function )
   `(implies (and (,inv-source n a) (integerp n))
	     (,inv-target (+ n -1) (,function n a))))

 (defun distributivity-function--1 (inv-source function  group-operation-source group-operation-target)
   `(implies (and (,inv-source n a)
		 (,inv-source n b)
		 (integerp n))
	    (equal (,function n (,group-operation-source n a b))
		   (,group-operation-target (+ n -1) (,function n a) (,function n b)))))

 (defun function-external-source--1 (inv-source inv-ring external-source external-target function )
   `(implies (and (,inv-source n a)
		  (,inv-ring r)
		  (integerp n))
	    (equal (,function n (,external-source n r a))
		   (,external-target (+ n -1) r (,function n a)))))

 (defun function-inverse--1 (inv-source inverse-source inverse-target function)
   `(implies (and (,inv-source n a) (integerp n))
	    (equal (,function n (,inverse-source n a))
		   (,inverse-target (+ n -1) (,function n a)))))

 (defun function-0--1 (function  zero-source zero-target)
   `(implies (integerp n)
	     (equal (,function n (,zero-source n))
		    (,zero-target (+ n -1)))))



(defun morphism-degree--1-condition (inv-source inv-target function  group-operation-source group-operation-target external-source external-target inv-ring
				      zero-source zero-target inverse-source inverse-target)
  (cons 'and 
	(cons (closure-function--1 inv-source inv-target function )
	      (cons (distributivity-function--1 inv-source function  group-operation-source group-operation-target)
		    (cons (function-external-source--1 inv-source inv-ring external-source external-target function )
			  (cons (function-0--1 function  zero-source zero-target)
				(cons (function-inverse--1 inv-source inverse-source inverse-target function)
				'nil)))))))


(defmacro defmorphism-degree--1 (inv-source inv-target function  group-operation-source group-operation-target external-source external-target inv-ring
				      zero-source zero-target inverse-source inverse-target name &key hints)
  (cons 'defthm 
	(cons (intern-in-package-of-symbol
	       (coerce (packn1 (list name "-is-a-morphism-of-degree--1"))
		       'string)
	       name)
	      (cons (morphism-degree--1-condition inv-source inv-target function  group-operation-source group-operation-target 
					external-source external-target inv-ring zero-source zero-target inverse-source inverse-target)
		    (IF HINTS (LIST :HINTS HINTS) NIL)))))


;;;***************************************************************************
;;;
;;; Morphism degree 0
;;;
;;;***************************************************************************

 
 (defun closure-function-0 (inv-source inv-target function )
   `(implies (and (,inv-source n a) (integerp n))
	     (,inv-target n (,function n a))))

 (defun distributivity-function-0 (inv-source function  group-operation-source group-operation-target)
   `(implies (and (,inv-source n a)
		 (,inv-source n b)
		 (integerp n))
	    (equal (,function n (,group-operation-source n a b))
		   (,group-operation-target n (,function n a) (,function n b)))))

 (defun function-external-source-0 (inv-source inv-ring external-source external-target function )
   `(implies (and (,inv-source n a)
		  (,inv-ring r)
		  (integerp n))
	    (equal (,function n (,external-source n r a))
		   (,external-target n r (,function n a)))))

 (defun function-0-0 (function  zero-source zero-target)
   `(implies (integerp n)
	     (equal (,function n (,zero-source n))
		    (,zero-target n))))

(defun function-inverse-0 (inv-source inverse-source inverse-target function)
   `(implies (and (,inv-source n a) (integerp n))
	    (equal (,function n (,inverse-source n a))
		   (,inverse-target n (,function n a)))))



(defun morphism-degree-0-condition (inv-source inv-target function  group-operation-source group-operation-target external-source external-target inv-ring
				      zero-source zero-target inverse-source inverse-target)
  (cons 'and 
	(cons (closure-function-0 inv-source inv-target function )
	      (cons (distributivity-function-0 inv-source function  group-operation-source group-operation-target)
		    (cons (function-external-source-0 inv-source inv-ring external-source external-target function )
			  (cons (function-0-0 function  zero-source zero-target)
				(cons (function-inverse-0 inv-source inverse-source inverse-target function )
				'nil)))))))


(defmacro defmorphism-degree-0 (inv-source inv-target function  group-operation-source group-operation-target external-source external-target inv-ring
				      zero-source zero-target inverse-source inverse-target name &key hints)
  (cons 'defthm 
	(cons (intern-in-package-of-symbol
	       (coerce (packn1 (list name "-is-a-morphism-of-degree-0"))
		       'string)
	       name)
	      (cons (morphism-degree-0-condition inv-source inv-target function  group-operation-source group-operation-target 
					external-source external-target inv-ring zero-source zero-target inverse-source inverse-target)
		    (IF HINTS (LIST :HINTS HINTS) NIL)))))


;;;***************************************************************************
;;;
;;; Morphism degree 1
;;;
;;;***************************************************************************

 
 (defun closure-function-1 (inv-source inv-target function)
   `(implies (and (,inv-source n a)(integerp n))
	     (,inv-target (+ n 1) (,function n a))))

 (defun distributivity-function-1 (inv-source function  group-operation-source group-operation-target)
   `(implies (and (,inv-source n a)
		 (,inv-source n b)
		 (integerp n))
	    (equal (,function n (,group-operation-source n a b))
		   (,group-operation-target (+ n 1) (,function n a) (,function n b)))))

 (defun function-external-source-1 (inv-source inv-ring external-source external-target function )
   `(implies (and (,inv-source n a)
		  (,inv-ring r)
		  (integerp n))
	    (equal (,function n (,external-source n r a))
		   (,external-target (+ n 1) r (,function n a)))))

 (defun function-0-1 (function  zero-source zero-target)
   `(implies (integerp n)
	     (equal (,function n (,zero-source n))
		    (,zero-target (+ n 1)))))

(defun function-inverse-1 (inv-source inverse-source inverse-target function)
   `(implies (and (,inv-source n a) (integerp n))
	    (equal (,function n (,inverse-source n a))
		   (,inverse-target (+ n 1) (,function n a)))))



(defun morphism-degree-1-condition (inv-source inv-target function  group-operation-source group-operation-target external-source external-target inv-ring
				      zero-source zero-target inverse-source inverse-target)
  (cons 'and 
	(cons (closure-function-1 inv-source inv-target function )
	      (cons (distributivity-function-1 inv-source function  group-operation-source group-operation-target)
		    (cons (function-external-source-1 inv-source inv-ring external-source external-target function )
			  (cons (function-0-1 function  zero-source zero-target)
				(cons (function-inverse-1 inv-source inverse-source inverse-target function)
				'nil)))))))


(defmacro defmorphism-degree-1 (inv-source inv-target function  group-operation-source group-operation-target external-source external-target inv-ring
				  zero-source zero-target inverse-source inverse-target name &key hints)
  (cons 'defthm 
	(cons (intern-in-package-of-symbol
	       (coerce (packn1 (list name "-is-a-morphism-of-degree-1"))
		       'string)
	       name)
	      (cons (morphism-degree-1-condition inv-source inv-target function  group-operation-source group-operation-target 
					external-source external-target inv-ring zero-source zero-target inverse-source inverse-target)
		    (IF HINTS (LIST :HINTS HINTS) NIL)))))



;;;***************************************************************************
;;;
;;; Differential
;;;
;;;***************************************************************************

(defun functionofunction (inv function zero-s)
  `(implies (and (,inv n a) (integerp n))
		  (equal (,function (1- n) (,function n a)) 
			 (,zero-s (1- (1- n))))))
 

(defun differential-condition (inv function  group-operation external inv-ring zero-s inverse)
  (cons 'and 
	(cons (morphism-degree--1-condition inv inv function group-operation group-operation external external inv-ring zero-s zero-s inverse inverse)
	      (cons (functionofunction inv function zero-s)
		    'nil))))


(defmacro defdifferential (inv function group-operation external inv-ring zero-s inverse name &key hints)
  (cons 'defthm 
	(cons (intern-in-package-of-symbol
	       (coerce (packn1 (list name "-is-a-differential"))
		       'string)
	       name)
	      (cons (differential-condition inv function group-operation external inv-ring zero-s inverse)
		    (IF HINTS (LIST :HINTS HINTS) NIL)))))


;;;***************************************************************************
;;;
;;; Chain Complex 
;;;
;;;***************************************************************************

(defun chain-complex-condition (inv-ring addition-ring zero-elem-ring inverse-ring product-ring unit-ring
				inv-cc group-operation-cc zero-elem-cc external-cc inverse-cc differential)
  (cons 'and 
	(cons (graded-r-module-condition inv-ring addition-ring zero-elem-ring inverse-ring product-ring unit-ring
					 inv-cc group-operation-cc zero-elem-cc external-cc inverse-cc)
	      (cons (differential-condition inv-cc differential group-operation-cc external-cc inv-ring zero-elem-cc inverse-cc)
		    'nil))))



(defmacro defchain-complex (inv-ring addition-ring zero-elem-ring inverse-ring product-ring unit-ring
				inv-cc group-operation-cc zero-elem-cc external-cc inverse-cc differential  name &key hints)
  (cons 'defthm 
	(cons (intern-in-package-of-symbol
	       (coerce (packn1 (list name "-is-a-chain-complex"))
		       'string)
	       name)
	      (cons (chain-complex-condition inv-ring addition-ring zero-elem-ring inverse-ring product-ring unit-ring
				inv-cc group-operation-cc zero-elem-cc external-cc inverse-cc differential )
		    (IF HINTS (LIST :HINTS HINTS) NIL)))))


	

#|

Example: Trivial Chain Complex

; The ring R

(defun inv-ring (a)
	  (integerp a))
 
 (defun addition-ring (a b)
	  (+ a b))

(defun product-ring (a b)
	  (* a b))

(defun inverse (a)
	  (- a))

 (defun zero-element nil
	  0)

  (defun unit nil
	  1)

 ; Graded R-module

 ;; Characteristic function
(defun inv-top (n a) 
	  (declare (ignore n))
	  (equal a 0))

(defun group-operation-top (n a b)
	  (declare (ignore n))
	  (+ a b))

(defun zero-top (n)
	  (declare (ignore n))
	  0)

 (defun external-top (n a b)
	  (declare (ignore n))
	  (* a b))

 (defun inverse-top (n a)
	  (declare (ignore n a))
	  0)


 ;; The differential
 (defun d-top (n a)
   (declare (ignore n a))
	  0)





(defchain-complex inv-ring addition-ring zero-element inverse product-ring unit
  inv-top group-operation-top zero-top external-top inverse-top d-top  trivial)


|#





;;;***************************************************************************
;;;
;;; Chain Complex morphism
;;;
;;;***************************************************************************


(defun function-is-ccm-degree-0 (inv-source d-source d-target function)
   `(implies (and (,inv-source n a) (integerp n))
	    (equal (,d-target n (,function n a))
		   (,function (1- n) (,d-source n a)))))


(defun function-is-ccm-degree-1 (inv-source d-source d-target function)
   `(implies (and (,inv-source n a) (integerp n))
	    (equal (,d-target (+ n 1) (,function n a))
		   (,function (1- n) (,d-source n a)))))


(defun chain-complex-morphism-degree-0-condition (inv-ring addition-ring zero-elem-ring inverse-ring product-ring unit-ring
						  inv-source group-operation-source zero-elem-source external-source 
						  inverse-source d-source 
						  inv-target group-operation-target zero-elem-target external-target 
						  inverse-target d-target 
						  function 

)
  (cons 'and 
	(cons (chain-complex-condition inv-ring addition-ring zero-elem-ring inverse-ring product-ring unit-ring
				       inv-source group-operation-source zero-elem-source external-source 
				       inverse-source d-source )
	      (cons (chain-complex-condition inv-ring addition-ring zero-elem-ring inverse-ring product-ring unit-ring
				       inv-target group-operation-target zero-elem-target external-target 
				       inverse-target d-target )
		    (cons (morphism-degree-0-condition inv-source inv-target function  group-operation-source group-operation-target
					      external-source external-target inv-ring zero-elem-source zero-elem-target inverse-source inverse-target)
			  (cons (function-is-ccm-degree-0 inv-source d-source d-target function)
				'nil))))))

(defun chain-complex-morphism-degree-1-condition (inv-ring addition-ring zero-elem-ring inverse-ring product-ring unit-ring
						  inv-source group-operation-source zero-elem-source external-source 
						  inverse-source d-source 
						  inv-target group-operation-target zero-elem-target external-target 
						  inverse-target d-target 
						  function 

)
  (cons 'and 
	(cons (chain-complex-condition inv-ring addition-ring zero-elem-ring inverse-ring product-ring unit-ring
				       inv-source group-operation-source zero-elem-source external-source 
				       inverse-source d-source )
	      (cons (chain-complex-condition inv-ring addition-ring zero-elem-ring inverse-ring product-ring unit-ring
				       inv-target group-operation-target zero-elem-target external-target 
				       inverse-target d-target )
		    (cons (morphism-degree-1-condition inv-source inv-target function  group-operation-source group-operation-target
					      external-source external-target inv-ring zero-elem-source zero-elem-target inverse-source inverse-target)
			  (cons (function-is-ccm-degree-1 inv-source d-source d-target function)
				'nil))))))


(defmacro defchain-complex-morphism-degree-0 (inv-ring addition-ring zero-elem-ring inverse-ring product-ring unit-ring
						  inv-source group-operation-source zero-elem-source external-source 
						  inverse-source d-source 
						  inv-target group-operation-target zero-elem-target external-target 
						  inverse-target d-target 
						  function name &key hints)
  (cons 'defthm 
	(cons (intern-in-package-of-symbol
	       (coerce (packn1 (list name "-is-a-chain-complex-morphism-of-degree-0"))
		       'string)
	       name)
	      (cons (chain-complex-morphism-degree-0-condition inv-ring addition-ring zero-elem-ring inverse-ring product-ring unit-ring
						  inv-source group-operation-source zero-elem-source external-source 
						  inverse-source d-source 
						  inv-target group-operation-target zero-elem-target external-target 
						  inverse-target d-target 
						  function)
		    (IF HINTS (LIST :HINTS HINTS) NIL)))))

(defmacro defchain-complex-morphism-degree-1 (inv-ring addition-ring zero-elem-ring inverse-ring product-ring unit-ring
						  inv-source group-operation-source zero-elem-source external-source 
						  inverse-source d-source 
						  inv-target group-operation-target zero-elem-target external-target 
						  inverse-target d-target 
						  function name &key hints)
  (cons 'defthm 
	(cons (intern-in-package-of-symbol
	       (coerce (packn1 (list name "-is-a-chain-complex-morphism-of-degree-0"))
		       'string)
	       name)
	      (cons (chain-complex-morphism-degree-1-condition inv-ring addition-ring zero-elem-ring inverse-ring product-ring unit-ring
						  inv-source group-operation-source zero-elem-source external-source 
						  inverse-source d-source 
						  inv-target group-operation-target zero-elem-target external-target 
						  inverse-target d-target 
						  function)
		    (IF HINTS (LIST :HINTS HINTS) NIL)))))









#|

Example: Trivial Chain Complex

; The ring R

(defun inv-ring (a)
	  (integerp a))
 
 (defun addition-ring (a b)
	  (+ a b))

(defun product-ring (a b)
	  (* a b))

(defun inverse (a)
	  (- a))

 (defun zero-element nil
	  0)

  (defun unit nil
	  1)

 ; Graded R-module

 ;; Characteristic function
(defun inv-top (n a) 
	  (declare (ignore n))
	  (equal a 0))

(defun group-operation-top (n a b)
	  (declare (ignore n))
	  (+ a b))

(defun zero-top (n)
	  (declare (ignore n))
	  0)

 (defun external-top (n a b)
	  (declare (ignore n))
	  (* a b))

 (defun inverse-top (n a)
	  (declare (ignore n a))
	  0)


 ;; The differential
 (defun d-top (n a)
   (declare (ignore n a))
	  0)


;; The function f

(defun f (n a)
  (declare (ignore n a))
	  0)





(defchain-complex-morphism inv-ring addition-ring zero-element inverse product-ring unit
  inv-top group-operation-top zero-top external-top inverse-top d-top 
  inv-top group-operation-top zero-top external-top inverse-top d-top 
  f 
  trivial-f)


|#




;;;***************************************************************************
;;;
;;; Reduction
;;;
;;;***************************************************************************


(defun fog (inv-bottom f g)
    `(implies (and (,inv-bottom n gnrt) (integerp n))
	     (equal (,f n (,g n gnrt))
		    gnrt)))

(defun hod+doh (inv-top group-operation-top h d-top inverse-top g f)
   `(implies (and (,inv-top n gnrt) (integerp n))
	    (equal (,group-operation-top n (,h (1- n) (,d-top n gnrt))
		      (,d-top (1+ n) (,h n gnrt)))
		   (,group-operation-top n gnrt
		      (,inverse-top n (,g n (,f n gnrt)))))))
 
 (defun foh (inv-top f h zero-bottom)
   `(implies (and (,inv-top n gnrt) (integerp n))
	    (equal (,f (1+ n) (,h n gnrt))
		   (,zero-bottom (1+ n)))))

 (defun hog (inv-bottom h g zero-top)
   `(implies (and (,inv-bottom n gnrt) (integerp n))
	    (equal (,h n (,g n gnrt))
		   (,zero-top (1+ n)))))
  
 (defun hoh (inv-top h zero-top)
   `(implies (and (,inv-top n gnrt) (integerp n))
	    (equal (,h (1+ n) (,h n gnrt))
		   (,zero-top (1+ (1+ n))))))





(defun reduction-condition (inv-ring addition-ring zero-elem-ring inverse-ring product-ring unit-ring
						  inv-top group-operation-top zero-elem-top external-top 
						  inverse-top d-top 
						  inv-bottom group-operation-bottom zero-elem-bottom external-bottom 
						  inverse-bottom d-bottom 
						  f  g  h 

)
  (cons 'and 
	(cons (chain-complex-morphism-degree-0-condition inv-ring addition-ring zero-elem-ring inverse-ring product-ring unit-ring
						inv-top group-operation-top zero-elem-top external-top 
						inverse-top d-top 
						inv-bottom group-operation-bottom zero-elem-bottom external-bottom 
						inverse-bottom d-bottom 
						f )
	      (cons (morphism-degree-1-condition inv-top inv-top h  group-operation-top group-operation-top external-top external-top inv-ring zero-elem-top zero-elem-top inverse-top inverse-top)
		    (cons (chain-complex-morphism-degree-0-condition inv-ring addition-ring zero-elem-ring inverse-ring product-ring unit-ring
						inv-bottom group-operation-bottom zero-elem-bottom external-bottom 
						inverse-bottom d-bottom 
						inv-top group-operation-top zero-elem-top external-top 
						inverse-top d-top 
						g )
			  (cons (fog inv-bottom f g)
						  (cons (hod+doh inv-top group-operation-top h d-top inverse-top g f)
							(cons (foh inv-top f h zero-elem-bottom)
							      (cons (hog inv-bottom h g zero-elem-top)
								    (cons (hoh inv-top h zero-elem-top) 'nil))))))))))

(defmacro defreduction (inv-ring addition-ring zero-elem-ring inverse-ring product-ring unit-ring
						  inv-top group-operation-top zero-elem-top external-top 
						  inverse-top d-top 
						  inv-bottom group-operation-bottom zero-elem-bottom external-bottom 
						  inverse-bottom d-bottom
						  f g  h  name &key hints)
  (cons 'defthm 
	(cons (intern-in-package-of-symbol
	       (coerce (packn1 (list name "-is-a-reduction"))
		       'string)
	       name)
	      (cons (reduction-condition inv-ring addition-ring zero-elem-ring inverse-ring product-ring unit-ring
					 inv-top group-operation-top zero-elem-top external-top 
					 inverse-top d-top 
					 inv-bottom group-operation-bottom zero-elem-bottom external-bottom 
					 inverse-bottom d-bottom 
					 f  g  h )
		    (IF HINTS (LIST :HINTS HINTS) NIL))))) 





;;;***************************************************************************
;;;
;;; Homotopy Equivalence
;;;
;;;***************************************************************************


(defun homotopy-equivalence-condition (inv-ring addition-ring zero-elem-ring inverse-ring product-ring unit-ring
						inv-left group-operation-left zero-elem-left external-left 
						inverse-left d-left 
						inv-middle group-operation-middle zero-elem-middle external-middle 
						inverse-middle d-middle 
						inv-right group-operation-right zero-elem-right external-right 
						inverse-right d-right
						lf  lg  lh  rf  rg rh)
  (cons 'and 
	(cons (reduction-condition inv-ring addition-ring zero-elem-ring inverse-ring product-ring unit-ring
				   inv-middle group-operation-middle zero-elem-middle external-middle 
				   inverse-middle d-middle
				   inv-left group-operation-left zero-elem-left external-left 
				   inverse-left d-left 
				   lf  lg  lh)
	      (cons (reduction-condition inv-ring addition-ring zero-elem-ring inverse-ring product-ring unit-ring
				   inv-middle group-operation-middle zero-elem-middle external-middle 
				   inverse-middle d-middle
				   inv-right group-operation-right zero-elem-right external-right 
				   inverse-right d-right 
				   rf  rg  rh)
		    'nil))))



(defmacro defhomotopy-equivalence (inv-ring addition-ring zero-elem-ring inverse-ring product-ring unit-ring
						inv-left group-operation-left zero-elem-left external-left 
						inverse-left d-left 
						inv-middle group-operation-middle zero-elem-middle external-middle 
						inverse-middle d-middle 
						inv-right group-operation-right zero-elem-right external-right 
						inverse-right d-right
						lf  lg  lh  rf  rg rh  name &key hints)
  (cons 'defthm 
	(cons (intern-in-package-of-symbol
	       (coerce (packn1 (list name "-is-an-homotopy-equivalence"))
		       'string)
	       name)
	      (cons (homotopy-equivalence-condition inv-ring addition-ring zero-elem-ring inverse-ring product-ring unit-ring
						inv-left group-operation-left zero-elem-left external-left 
						inverse-left d-left 
						inv-middle group-operation-middle zero-elem-middle external-middle 
						inverse-middle d-middle 
						inv-right group-operation-right zero-elem-right external-right 
						inverse-right d-right
						lf  lg  lh  rf  rg rh)
		    (IF HINTS (LIST :HINTS HINTS) NIL)))))